package nsalt.fetch.branch

import chisel3._
import chisel3.util._

import chiselFv._

class AsyncReadMem(val entryCount: Int) extends Module with Formal {

  val io = IO(new Bundle {

    val in = Flipped(new Bundle {
      val saveAble = Output(Bool())
      val plus = Output(Bool())
      val addr = Output(UInt(log2Up(entryCount).W))
      val data = Output(UInt(2.W))
    })

    val out = Output(UInt(2.W))

  })
 
  val mem = Mem(entryCount, UInt(2.W))
 
  val spec = io.in
  val specOrig = RegNext(spec)
  val dataOrig = RegNext(mem.read(spec.addr))

  when (specOrig.saveAble) {
    when (specOrig.plus && (dataOrig =/= "b11".U)){
      mem.write(specOrig.addr, dataOrig + 1.U);
    }.elsewhen (!specOrig.plus&& (dataOrig =/= "b00".U)){
      mem.write(specOrig.addr, dataOrig - 1.U);
    }
  }

  io.out := mem.read(io.in.addr)
  
  // FOR FORMAL VERIFICATION


  // val specPrev = ShiftRegister(io.in, 2)
  // val dataCurr = RegNext(mem.read(spec.addr))

  // val memReadPrev = ShiftRegister(mem.read(io.in.addr), 2)

  // val memReadCurr = mem.read(specPrev.addr)

  // assert(dataOrig === dataCurr)
  // assert(RegNext(RegNext(dataOrig)) === ShiftRegister(dataOrig, 2))
  // assert(RegNext(dataOrig) === RegNext(dataCurr))

  // when(RegNext(specOrig).saveAble) {
  //   when (RegNext(specOrig).plus && (RegNext(dataCurr) =/= "b11".U)) {
  //     assert(mem.read(RegNext(specOrig).addr) === RegNext(dataCurr) + 1.U)
  //   }
  // }


}


